-----------------------------------------------------------------------------
--
-- Module      :  Data.TypeLevel.List
-- Copyright   :
-- License     :  AllRightsReserved
--
-- Maintainer  :  eduard.sergeev@gmail.com
-- Stability   :  Highly Experimental
-- Portability :
--
-- Type-level list
--
-----------------------------------------------------------------------------

{-# LANGUAGE NoImplicitPrelude, TypeFamilies, TypeOperators, UndecidableInstances #-}


module Data.TypeLevel.List (

   (:::),
   Nil,

   Length,
   
   (:==:),
   (:/=:),

   Compare,
   (:<=:),

) where

import Data.TypeLevel.Families
import Data.TypeLevel.Boolean
import Data.TypeLevel.Peano

infixr 4 :::

data x ::: xs
data Nil

type family Length l :: *
type instance Length Nil = Zero
type instance Length (x ::: xs) = Succ (Length xs)


-- * Type-level "Eq" implementation
type instance Nil :==: Nil = True 
type instance Nil :==: (rx ::: rxs) = False
type instance (lx ::: lxs) :==: Nil = False 
type instance (lx ::: lxs) :==: (rx ::: rxs) = (lx :==: rx) :*: (lxs :==: rxs) 

type instance l :/=: r = Not (l :==: r) 


-- * Type-level "Ord" implementation
type instance Compare Nil Nil = EQ
type instance Compare (lx ::: lxs) Nil = GT
type instance Compare Nil (rx ::: rxs) = LT
type instance Compare (lx ::: lxs) (rx ::: rxs) = Comb (Compare lx rx) (Compare lxs rxs)

type family Comb l r :: *
type instance Comb LT r = LT
type instance Comb GT r = GT
type instance Comb EQ r = r


type instance Nil :<=: Nil = True
type instance (lx ::: lxs) :<=: Nil = True
type instance Nil :<=: (rx ::: rxs) = False
type instance (lx ::: lxs) :<=: (rx ::: rxs) = (lx :<=: rx) :*: (lxs :<=: rxs)